from django.db import models

from tppt.lib import Model
from tppt.lib.db import Actions
from tppt.lib import utils

class Division(Model):
	short = models.CharField(max_length=20, primary_key=True)
	name = models.CharField(max_length=200)
	description = models.TextField(blank=True)

	class Admin:
		list_display=('short', 'name')
	
	class Actions(Actions):
		inner_objects=('AxiomFamily', 'division')

class AxiomFamily(Model):
	short = models.CharField(max_length=20, primary_key=True)
	division = models.ForeignKey(Division)
	name = models.CharField(max_length=200)

	class Meta:
		verbose_name_plural='axiom families'
	class Admin:
		list_display=('short', 'name')
	class Actions(Actions):
		inner_objects=('AxiomSet', 'family')

class AxiomSet(Model):
	short = models.CharField(max_length=20,primary_key=True)
	family = models.ForeignKey(AxiomFamily)
	name = models.CharField(max_length=200)

	class Admin:
		list_display=('short', 'name')

class ProblemStatus(Model):
	name = models.CharField(max_length=40,primary_key=True)
	abbr = models.CharField(max_length=200)
	theorem = models.BooleanField()
	unknown = models.BooleanField()

	class Meta:
		verbose_name_plural='problem statuses'
	class Admin:
		list_display=('name', 'theorem', 'unknown')

class ProblemFamily(Model):
	short = models.CharField(max_length=20,primary_key=True)
	division = models.ForeignKey(Division)
	class Admin:
		pass

class Problem(Model):
	short = models.CharField(max_length=20,primary_key=True)
	division = models.ForeignKey(Division)
	family = models.ForeignKey(ProblemFamily)
	name = models.CharField(max_length=200)
	status = models.ForeignKey(ProblemStatus)
	axioms = models.ManyToManyField(AxiomSet)
	formula_count = models.IntegerField(blank=True, null=True)
	atom_count = models.IntegerField(blank=True, null=True)
	predicate_count = models.IntegerField(blank=True, null=True)
	functor_count = models.IntegerField(blank=True, null=True)

	
	class Admin:
		list_display=('short', 'status', 'name')
		list_filter=('status','division')
	class Actions(Actions):
		inner_objects=('Result', 'problem')
	
class ProblemGroup(Model):
	name = models.CharField(max_length=50,primary_key=True)
	problems = models.ManyToManyField(Problem)

	class Admin:
		pass
	
	
class ProverClass(Model):
	short = models.CharField(max_length=20,primary_key=True)
	name = models.CharField(max_length=200)
	added = models.DateTimeField(auto_now_add=True)

	class Meta:
		verbose_name_plural='prover classes'
	class Admin:
		pass

class ProverVersion(Model):
	short = models.CharField(max_length=20,primary_key=True)
	prover = models.ForeignKey(ProverClass)
	version = models.CharField(max_length=20)
	hash = models.CharField(max_length=200)
	added = models.DateTimeField(auto_now_add=True)

	class Admin:
		pass

class OutputFormat(Model):
	name = models.CharField(max_length=20,primary_key=True)

	class Admin:
		pass

class ProverInstance(Model):
	short = models.CharField(max_length=20,primary_key=True)
	engine = models.ForeignKey(ProverVersion)
	output_format = models.ForeignKey(OutputFormat, blank=True, null=True)
	command_line = models.CharField(max_length=500)
	time_limit = models.IntegerField()
	added = models.DateTimeField(auto_now_add=True)

	class Admin:
		list_display=('short', 'engine', 'time_limit', 'output_format')


class TPTPVersion(Model):
	short = models.CharField(max_length=20,primary_key=True)
	version = models.CharField(max_length=20)
	default = models.BooleanField()

	class Meta:
		verbose_name='TPTP version'
	class Admin:
		pass

class CPUFamily(Model):
	short = models.CharField(max_length=20, primary_key=True)
	name = models.CharField(max_length=200)
	
	class Meta:
		verbose_name='CPU family'
		verbose_name_plural='CPU families'
	class Admin:
		pass

class OS(Model):
	short = models.CharField(max_length=20,primary_key=True)
	name = models.CharField(max_length=200)
	version = models.CharField(max_length=20)
	arch = models.CharField(max_length=20)
	
	class Meta:
		verbose_name='operating system'
		verbose_name_plural='operating systems'
	class Admin:
		pass

class Computer(Model):
	short = models.CharField(max_length=20,primary_key=True)
	name = models.CharField(max_length=200)
	cpu = models.ForeignKey(CPUFamily)
	os = models.ForeignKey(OS)
	cpu_frequency = models.IntegerField()
	ram = models.IntegerField()
	bench_coef = models.FloatField(null=True, blank=True)
	added = models.DateTimeField(auto_now_add=True)

	class Admin:
		pass

class ResultType(Model):
	name = models.CharField(max_length=40,primary_key=True)
	proved = models.BooleanField()
	refuted = models.BooleanField()
	time_out = models.BooleanField()

	class Admin:
		pass
	
class ResultEvaluation(Model):
	problem_status = models.ForeignKey(ProblemStatus)
	result_type = models.ForeignKey(ResultType)
	ok = models.BooleanField()
	wrong = models.BooleanField()
	discovery = models.BooleanField()
	fail = models.BooleanField()

	def __unicode__(self):
		return "(%s vs. %s)" % (self.problem_status, self.result_type)
	class Admin:
		pass

class Result(Model):
	problem = models.ForeignKey(Problem)
	prover = models.ForeignKey(ProverInstance)
	result_type = models.ForeignKey(ResultType)
	tptp = models.ForeignKey(TPTPVersion)
	computer = models.ForeignKey(Computer, blank=True, null=True)
	time = models.FloatField()
	added = models.DateTimeField(auto_now_add=True)
	
	def get_details_sections(self):
		from tppt.lib.actions.model.details import ReferringEntitiesSection
		from tppt.data.details import ResultDetailsSection 
		res=super(Result, self).get_details_sections()
		res=utils.filter(lambda x:not isinstance(x, ReferringEntitiesSection) or x.ref_model!=ResultDetail, res)
		res.append(ResultDetailsSection())
		return res
	def __unicode__(self):
		return "(%s, %s -> %s)" % (self.problem, self.prover, self.result_type)
	class Admin:
		pass

class DataType(Model):
	short = models.CharField(max_length=20,primary_key=True)

	class Admin:
		pass
	
class ResultDetailType(Model):
	short = models.CharField(max_length=50,primary_key=True)
	data_type = models.ForeignKey(DataType)
	name = models.CharField(max_length=200)

	class Admin:
		pass
	
class ResultDetail(Model): 
	detail_type = models.ForeignKey(ResultDetailType)
	result = models.ForeignKey(Result)
	value = models.CharField(max_length=400)

	def __unicode__(self):
		return "(%s: %s)" % (self.detail_type, self.value)
	class Admin:
		pass

class Proof(Model):
	origin = models.ForeignKey(Result,primary_key=True)
	text = models.TextField()

	class Admin:
		pass
	
class PublishedFile(Model):
	name = models.CharField(max_length=50, primary_key=True)
	title = models.CharField(max_length=200)
	content = models.TextField()
	added = models.DateTimeField(auto_now_add=True)

	class Admin:
		pass
	
class ProverProblemAnalysis(Model):
	name = models.CharField(max_length=200, primary_key=True)
	provers = models.ManyToManyField(ProverInstance)
	problem_groups = models.ManyToManyField(ProblemGroup)

	class Meta:
		verbose_name='prover-problem analysis'
		verbose_name_plural='prover-problem analyses'
	class Admin:
		list_display=('name',)
